package form;

import java.awt.event.ActionEvent;
import java.awt.event.ActionListener;
import java.io.ByteArrayInputStream;
import java.io.File;
import java.io.FileInputStream;
import java.io.FileOutputStream;
import java.io.IOException;
import java.io.InputStream;
import java.io.ObjectInputStream;
import java.io.ObjectOutputStream;
import java.util.Iterator;

import javax.swing.BorderFactory;
import javax.swing.BoxLayout;
import javax.swing.JCheckBoxMenuItem;
import javax.swing.JFileChooser;
import javax.swing.JFrame;
import javax.swing.JMenu;
import javax.swing.JMenuBar;
import javax.swing.JMenuItem;
import javax.swing.JOptionPane;
import javax.swing.JPanel;
import javax.swing.JScrollPane;
import javax.swing.JSeparator;
import javax.swing.JTextArea;
import javax.swing.WindowConstants;
import javax.swing.filechooser.FileFilter;

import proposition.Proposition;
import resolution.KnowlegdeBase;
import resolution.ProverController;
import data.DataPrintStream;
import data.DataPrinter;

public class ProverForm extends javax.swing.JFrame implements DataPrinter {

	private static final long serialVersionUID = 1L;

	private JMenuItem jMenuItemProve;

	private JMenu jMenuTheorem;

	private JMenuItem deleteMenuItem;

	private JSeparator jSeparator1;

	private JMenuItem pasteMenuItem;

	private JTextArea jTextAreaStatus;

	private JTextArea jTextAreaProposition;

	private JScrollPane jScrollPane2;

	private JScrollPane jScrollPane1;

	private JPanel jPanel2;

	private JPanel jPanel1;

	private JCheckBoxMenuItem jCheckBoxMenuInfo;

	private JMenuItem compileBaseMenuItem;

	private JMenuItem copyMenuItem;

	private JMenuItem exitMenuItem;

	private JSeparator jSeparator2;

	private JMenuItem closeFileMenuItem;

	private JMenuItem saveAsMenuItem;

	private JMenuItem saveMenuItem;

	private JMenuItem openFileMenuItem;

	private JMenu jMenuBase;

	private JMenuBar jMenuBar1;

	private ProverController controller = new ProverController();

	private boolean detailedInfo = false;

	public ProverForm() {
		super();
		initGUI();
		DataPrintStream.setDataPrinter(this);
	}

	private void initGUI() {
		try {
			{
				this.setTitle("Provador Automático para Lógica Proposicional");
				this.setFocusTraversalKeysEnabled(false);
				BoxLayout thisLayout = new BoxLayout(getContentPane(),
						javax.swing.BoxLayout.Y_AXIS);
				getContentPane().setLayout(thisLayout);
				this.setExtendedState(JFrame.MAXIMIZED_BOTH);
				this.setDefaultCloseOperation(WindowConstants.EXIT_ON_CLOSE);
				{
					jPanel1 = new JPanel();
					BoxLayout jPanel1Layout = new BoxLayout(jPanel1,
							javax.swing.BoxLayout.Y_AXIS);
//					getContentPane().add(jPanel1);
					jPanel1.setBounds(14, 14, 567, 147);
					jPanel1.setBorder(BorderFactory
							.createTitledBorder("Gram�tica"));
					jPanel1.setLayout(jPanel1Layout);
					{
						jScrollPane1 = new JScrollPane();
						jPanel1.add(jScrollPane1);
						jScrollPane1.setBounds(7, 21, 553, 119);
						{
							jTextAreaProposition = new JTextArea();
							jScrollPane1.setViewportView(jTextAreaProposition);
							jTextAreaProposition.setFont(new java.awt.Font(
									"Tahoma", 0, 16));
							String gramatica;
							gramatica = "Sigma = {a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z,\n"
									+ " A, B, C, D, E, F, G, H, I, J, K, L, M, N, O, P, Q, R, S, T, U, V, W, X, Y, Z,\n "
									+ " 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,\n "
									+ " +, -, =, *, /, >, <, (, ), ->, <->, &&, ||, ~, \\, } \n "
									+ "N = {CARACTERE, LITERAL, PROP1, PROP2, PROP3, PROP4, PROP5, LISTA_PROPS} \n"
									+ "S = {LISTA_PROP}\n "
									+ "P ={CARACTERE->a|b|c|d|e|f|g|h|i|j|k|l|m|n|o|p|q|r|s|t|u|v|w|x|y|z|\n"
									+ "A|B|C|D|E|F|G|H|I|J|K|L|M|N|O|P|Q|R|S|T|U|V|W|X|Y|Z| \n"
									+ "0|1|2|3|4|5|6|7|8|9|+|-|=|*|/|>|>=|<|<=, \n"
									+ "LITERAL->CARACTERE|LITERAL.CARACTERE|~.LITERAL, \n"
									+ "PROP1->LITERAL|PROP5|(.PROP5.),\n"
									+ "PROP2->PROP1|PROP2.||.PROP1,\n"
									+ "PROP3->PROP2|PROP3.&&.PROP2,\n"
									+ "PROP4->PROP3|PROP4.<->.PROP3,\n"
									+ "PROP5->PROP4|PROP5.->.PROP4,\n"
									+ "LISTA_PROPS->PROP5|LISTA_PROPS.\\,.PROP5";
							jTextAreaProposition.setText(gramatica);
						}
					}
				}

				{
					jPanel1 = new JPanel();
					BoxLayout jPanel1Layout = new BoxLayout(jPanel1,
							javax.swing.BoxLayout.Y_AXIS);
					getContentPane().add(jPanel1);
					jPanel1.setBounds(14, 14, 567, 147);
					jPanel1.setBorder(BorderFactory
							.createTitledBorder("Proposição"));
					jPanel1.setLayout(jPanel1Layout);
					{
						jScrollPane1 = new JScrollPane();
						jPanel1.add(jScrollPane1);
						jScrollPane1.setBounds(7, 21, 553, 119);
						{
							jTextAreaProposition = new JTextArea();
							jScrollPane1.setViewportView(jTextAreaProposition);
							jTextAreaProposition.setFont(new java.awt.Font(
									"Tahoma", 0, 16));
						}
					}
				}
				{
					jPanel2 = new JPanel();
					BoxLayout jPanel2Layout = new BoxLayout(jPanel2,
							javax.swing.BoxLayout.Y_AXIS);
					getContentPane().add(jPanel2);
					jPanel2.setBounds(14, 175, 567, 112);
					jPanel2.setBorder(BorderFactory
							.createTitledBorder("Resultado"));
					jPanel2.setLayout(jPanel2Layout);
					{
						jScrollPane2 = new JScrollPane();
						jPanel2.add(jScrollPane2);
						jScrollPane2.setBounds(7, 21, 553, 84);
						jScrollPane2.setAutoscrolls(true);
						jScrollPane2.getVerticalScrollBar()
								.setAutoscrolls(true);
						{
							jTextAreaStatus = new JTextArea();
							jScrollPane2.setViewportView(jTextAreaStatus);
							jTextAreaStatus.setFont(new java.awt.Font("Tahoma",
									0, 16));
						}
					}
				}

			}
			this.setSize(603, 353);
			{

				jMenuBar1 = new JMenuBar();
				setJMenuBar(jMenuBar1);
				{
					jMenuBase = new JMenu();
					jMenuBar1.add(jMenuBase);
					jMenuBase.setText("Base");
					{
						openFileMenuItem = new JMenuItem();
						jMenuBase.add(openFileMenuItem);
						openFileMenuItem.setText("Abrir arquivo de Base de Conhecimento");
						openFileMenuItem
								.addActionListener(new ActionListener() {
									public void actionPerformed(ActionEvent evt) {
										openFileMenuItemActionPerformed(evt);
									}
								});
					}
					{
						saveMenuItem = new JMenuItem();
						jMenuBase.add(saveMenuItem);
						saveMenuItem.setText("Salvar a Base de Conhecimento atual para arquivo");
						saveMenuItem
								.addActionListener(new ActionListener() {
									public void actionPerformed(ActionEvent evt) {
										saveMenuItemActionPerformed(evt);
									}
								});
					}
					{
						compileBaseMenuItem = new JMenuItem();
						jMenuBase.add(compileBaseMenuItem);
						compileBaseMenuItem.setText("Compilar as proposições para Base de Conhecimento");
						compileBaseMenuItem
								.addActionListener(new ActionListener() {
									public void actionPerformed(ActionEvent evt) {
										compileBaseMenuItemActionPerformed(evt);
									}
								});
					}
				}
				{
					jMenuTheorem = new JMenu();
					jMenuBar1.add(jMenuTheorem);
					jMenuTheorem.setText("Teorema");
					{
						jMenuItemProve = new JMenuItem();
						jMenuTheorem.add(jMenuItemProve);
						jMenuItemProve.setText("Provar");
						jMenuItemProve.addActionListener(new ActionListener() {
							public void actionPerformed(ActionEvent evt) {
								jMenuItemProveActionPerformed(evt);
							}
						});
					}
					{
						jSeparator1 = new JSeparator();
						jMenuTheorem.add(jSeparator1);
					}
					{
						jCheckBoxMenuInfo = new JCheckBoxMenuItem();
						jMenuTheorem.add(jCheckBoxMenuInfo);
						jCheckBoxMenuInfo.setText("Detalhes");
						jCheckBoxMenuInfo
								.addActionListener(new ActionListener() {
									public void actionPerformed(ActionEvent evt) {
										jCheckBoxMenuInfoActionPerformed(evt);
									}
								});
					}
				}
			}
		} catch (Exception e) {
			e.printStackTrace();
		}
	}

	public void write(int b) throws IOException {
		this.jTextAreaStatus.append(new Character((char) b).toString());
	}

	private void cutMenuItemActionPerformed(ActionEvent evt) {
	}

	private void compileBaseMenuItemActionPerformed(ActionEvent evt) {
		if (jTextAreaProposition.getText().length() == 0) {
			JOptionPane.showMessageDialog(this, "Sem dados para carregar.\nDigite os teoremas da base de conhecimento\nna área de Proposições e tente novamente.",
					"Erro", JOptionPane.ERROR_MESSAGE);
			return;
		}

		byte[] array = this.jTextAreaProposition.getText().getBytes();
		final InputStream is = new ByteArrayInputStream(array);
		new Thread() {
			public void run() {
				try {
					jTextAreaStatus.setText("");
					DataPrintStream
							.println("Compilando as proposicoes da base...");
					if (!controller.compileBase(is))
						return;
					DataPrintStream.println("Compilado com sucesso !");
					DataPrintStream.println("Porposicoes aceitas: ");
					Iterator<Proposition> iterator = controller
							.getLastPropositions().iterator();
					DataPrintStream.println();
					while (iterator.hasNext()) {
						Proposition proposition = iterator.next();
						DataPrintStream.println("\tOriginal : "
								+ proposition.getOriginalProposition());
						DataPrintStream.println("\tForma Normal Conjuntiva: "
								+ proposition);
						DataPrintStream.println();
					}
				} catch (Exception e) {
					e.printStackTrace(DataPrintStream.out);
				}
			}
		}.start();
	}

	private void saveMenuItemActionPerformed(ActionEvent evt) {
		JFileChooser fileChooser = new JFileChooser();

		fileChooser.setFileFilter(new FileFilter() {
			public boolean accept(File file) {
				return file.getName().toLowerCase().endsWith(".peb");
			}

			public String getDescription() {
				return "Arquivo";
			}
		});

		fileChooser.setFileSelectionMode(JFileChooser.FILES_ONLY);
		int result = fileChooser.showSaveDialog(this);

		if (result == JFileChooser.CANCEL_OPTION)
			return;

		File file = fileChooser.getSelectedFile();
		if (file == null || file.getName().equals(""))
			JOptionPane.showMessageDialog(this, "Erro no nome do arquivo",
					"Erro no nome do arquivo", JOptionPane.ERROR_MESSAGE);
		else {
			try {
				ObjectOutputStream os = new ObjectOutputStream(
						new FileOutputStream(file));
				KnowlegdeBase base = controller.getBase();
				os.writeObject(base);
			} catch (IOException e) {
				JOptionPane.showMessageDialog(this, "Erro ao salvar", "Erro", JOptionPane.ERROR_MESSAGE);
				e.printStackTrace(DataPrintStream.out);
			}
		}
	}

	private void jMenuItemProveActionPerformed(ActionEvent evt) {
		if (jTextAreaProposition.getText().length() == 0) {
			JOptionPane.showMessageDialog(this, "Sem dados para provar",
					"Erro", JOptionPane.ERROR_MESSAGE);
			return;
		}

		byte[] array = this.jTextAreaProposition.getText().getBytes();
		final InputStream is = new ByteArrayInputStream(array);
		new Thread() {
			public void run() {
				try {
					jTextAreaStatus.setText("");
					DataPrintStream.println("Compilando os teoremas.");
					controller.compileTheorem(is);
					DataPrintStream.println("Compilacao feita com sucesso!");
					DataPrintStream.println("Proposicoes carregadas:");
					Iterator<Proposition> iterator = controller
							.getLastPropositions().iterator();
					DataPrintStream.println();
					while (iterator.hasNext()) {
						Proposition proposition = iterator.next();
						DataPrintStream.println("\tProposicao: " + proposition);
						DataPrintStream.println();
					}
					controller.proveTheorems();
				} catch (Exception e) {
					e.printStackTrace(DataPrintStream.out);
				}
			}
		}.start();
	}

	private void openFileMenuItemActionPerformed(ActionEvent evt) {
		JFileChooser fileChooser = new JFileChooser();

		fileChooser.setFileFilter(new FileFilter() {
			public boolean accept(File file) {
				return file.getName().toLowerCase().endsWith(".peb");
			}

			public String getDescription() {
				return "Base de Conhecimento (.peb)";
			}
		});

		fileChooser.setFileSelectionMode(JFileChooser.FILES_ONLY);
		int result = fileChooser.showOpenDialog(this);

		if (result == JFileChooser.CANCEL_OPTION)
			return;

		File file = fileChooser.getSelectedFile();
		if (file == null || file.getName().equals(""))
			JOptionPane.showMessageDialog(this, "Erro no nome do arquivo",
					"Erro no nome do arquivo", JOptionPane.ERROR_MESSAGE);
		else {
			try {
				ObjectInputStream is = new ObjectInputStream(
						new FileInputStream(file));
				KnowlegdeBase base = (KnowlegdeBase) is.readObject();
				controller.setCompiledBase(base);
				DataPrintStream.println("Compilando base");
				DataPrintStream.println("Proposicoes:");
				DataPrintStream.println();
				Iterator<Proposition> iterator = base.getPropositions()
						.iterator();
				while (iterator.hasNext()) {
					Proposition proposition = iterator.next();
					DataPrintStream.println("\tOriginal: "
							+ proposition.getOriginalProposition());
					DataPrintStream.println("\tForma Normal Conjuntiva: "
							+ proposition);
					DataPrintStream.println();
				}
			} catch (IOException e) {
				JOptionPane.showMessageDialog(this, "Erro ao abrir o arquivo",
						"Error", JOptionPane.ERROR_MESSAGE);
				e.printStackTrace(DataPrintStream.out);
			} catch (ClassNotFoundException e) {
				JOptionPane.showMessageDialog(this, "Arquivo nao valido.",
						"Error", JOptionPane.ERROR_MESSAGE);
				e.printStackTrace(DataPrintStream.out);
			}
		}

	}

	private void jCheckBoxMenuInfoActionPerformed(ActionEvent evt) {
		detailedInfo = !detailedInfo;
		controller.printDetailedInfo(detailedInfo);
	}
}
